/*
**************************************************************************************************************
File:         ddr3_assertions.sv
Description:  Defines the assertions used in verifying the DDR3 interface
Author     :  Katerina Gleeson
              Rohit Kulkarni
              Aditya Joshi
**************************************************************************************************************
*/
`include "package.sv"

module ddr3_assertions(DDR_bus IF);
  
  //Property to verify RAS signal transitions during activate
  property RASL2RASH;
   @(posedge IF.CK)
     $fell(IF.RAS) |-> ##(tRCD) $rose(IF.RAS);
  endproperty
  RASL2RASH_1: assert property(RASL2RASH)  
  else
    $error("Violated tRCD requirement");
        
  //Property to verify CAS signal transitions during Read/Write    
  property CASL2CASH;                           //verify CAS fall and rise time
   @(posedge IF.CK)
  	$fell(IF.CAS) |-> ##tCL $rose(IF.CAS);
  endproperty
  CASL2CASH_1: assert property(CASL2CASH)
  else 
    $error("Violated tCL requirement");

  //Property to verify time between RAS going low in activate and data changing on DQ
  property RASL2DOUT;                           
   @(posedge IF.CK)
  	(DDR_controller.State == ACTIVATE && $fell(IF.RAS)) 
  	       |-> ##(tRCD + tCL) $changed(IF.DQ);
  endproperty
  RASL2DOUT_1: assert property(RASL2DOUT)
  else 
    $error("Violated tRCD + tCL requirement");
    

  //Property to verify read to precharge time    
  property Read2Precharge;                        
   @(posedge IF.CK)
  	($fell(IF.CAS) && $rose(IF.RAS))|-> ##(tCL + tDout) 
  	           ($fell(IF.RAS) && DDR_controller.State == PRECHARGE);
  endproperty
  Read2Precharge_1: assert property(Read2Precharge)
  else 
    $error("Violated tCL + tDout requirement");


 property BURST;   //test data bursts for rising and falling clock edges for burst cycle
    $changed (IF.DQ)  [*tDout] |-> ##tDout $isunknown(IF.DQ);
 endproperty
 BURST_1: assert property (@(posedge IF.CK) BURST)
 else
    $error("Violated Rising-Edge Burst length requirement");  
 BURST_2: assert property (@(negedge IF.CK) BURST)
 else   
    $error("Violated Falling-Edge Burst length requirement");


 property ACT2RD; //verify tRAS time between ACT and following PRE
   @(posedge IF.CK)
	 (DDR_controller.State == ACTIVATE && DDR_controller.OP == 0) 
	         |-> ##tRCD (DDR_controller.State == READ);
 endproperty
 ACT2RD_1: assert property(ACT2RD)
   else $error ("Violated ACTIVATE to READ delay");


 property ACT2PRE;
   @(posedge IF.CK)
   (DDR_controller.State == ACTIVATE)
       |-> ##tRAS (DDR_controller.State == PRECHARGE);
 endproperty  
 ACT2PRE_1: assert property (ACT2PRE)
   else $error("Violated tRAS Delay");


 property ACT2WR; //verify tRAS time between ACT and following PRE
   @(posedge IF.CK)
	 (DDR_controller.State == ACTIVATE && DDR_controller.OP == 1) 
	         |-> ##tRCD (DDR_controller.State == WRITE);
 endproperty
 ACT2WR_1: assert property(ACT2WR)
   else $error ("Violated ACTIVATE to WRITE delay");


 property ACTIVATE_PROP;
   @(posedge IF.CK)
   (DDR_controller.State == ACTIVATE) |-> ##0 ($fell(IF.RAS));
 endproperty
 ACTIVATE_1: assert property (ACTIVATE_PROP)
    else $error("Violated Activate initiation");

 property RAS2CAS;  //Verify that CAS falls tRCD after RAS during activate.
	 @(posedge IF.CK)
	 (DDR_controller.State == ACTIVATE && $fell(IF.RAS)) |-> ##(tRCD) $fell(IF.CAS);
 endproperty
 RAS2CAS_1: assert property (RAS2CAS)
  else $info("Violated RAS to CAS delay");


 property BURST_ONLY;
   @(posedge IF.CK)
	 $changed(IF.DQ) |-> ##tDout $isunknown(IF.DQ);
 endproperty
 BURST_ONLY_1: assert property (BURST_ONLY)
   else $info("Burst length Violation");
    

 property PRE_RAS;
   @(posedge IF.CK)
   (DDR_controller.State == PRECHARGE && $fell(IF.RAS) && IF.CS == 0) 
        |-> ##tRP  ($rose(IF.RAS) && $stable(IF.CAS));
 endproperty
 PRE_RAS_1: assert property (PRE_RAS)
    else $error("Violated Precharge Delay sequence");


 property WE_AND_DQ;
   @(posedge IF.CK)
   ($rose(IF.CAS) && $fell(IF.WE) && $changed(IF.DQ)) |-> ##tDout ($rose(IF.WE) && $isunknown(IF.DQ));
 endproperty
 WE_AND_DQ_1: assert property (WE_AND_DQ)
   else $error("Violated Write Enable and DQ hold time");

 property PRECHARGE_PROP;
    @(posedge IF.CK)
    (DDR_controller.State == PRECHARGE) |-> ##0 ($fell(IF.RAS) && $stable(IF.CAS));
endproperty
PRECHARGE_1: assert property (PRECHARGE_PROP)
  else $error("Violated precharge initiation");
    
    
property REF_XX;   //verify that autorefresh makes address x's, and cycles at tRFC.
  (DDR_controller.State == AUTO_REFRESH && $isunknown(IF.addr))
        |-> ##tRFC  (DDR_controller.State == AUTO_REFRESH && $isunknown(IF.addr));
endproperty  
assert property(@(posedge IF.CK) REF_XX);
     //tRFC needs to be created as parameter  
  
endmodule